<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<html>
<head>
<!--

  @(#)overview.html

-->
</head>
<body bgcolor="white">

Jchecker是一个软件模型检测工具。它可以针对类C源程序进行模型可达性检测。当发现可达的错误时，它会提示错误并给出相应的错误路径。如果所有的错误路径都不可达，Jchecker则会提示检测通过，在此情况下，程序的正确性得到了确保。

<h2>Package Specification</h2>

有关Jchecker的具体描述请参考以下文章：
<ul>
  <li><a href="Jchecker理论、方法与实现.doc">Jchecker理论、方法与实现</a> 
</ul>

<h2>Related Documentation</h2>

有关Jchecker设计的其他资料：
<ul>
  <li><a href="Jchecker UML graph.vsd">Jchecker设计类图</a>
</ul>

<!-- Put @see and @since tags down here. -->

</body>
</html>
